; benchmark generated from python API
(set-info :status unknown)
(declare-fun title_bg_feasible () Bool)
(declare-fun title_bg_width () Real)
(declare-fun title_bg_kid_16_width () Real)
(declare-fun title_bg_kid_16_x () Real)
(declare-fun title_bg_kid_16_feasible () Bool)
(declare-fun title_bg_kid_15_width () Real)
(declare-fun title_bg_kid_15_x () Real)
(declare-fun title_bg_kid_15_feasible () Bool)
(declare-fun title_bg_kid_14_width () Real)
(declare-fun title_bg_kid_14_x () Real)
(declare-fun title_bg_kid_14_feasible () Bool)
(declare-fun title_bg_kid_13_x () Real)
(declare-fun title_bg_kid_13_width () Real)
(declare-fun title_bg_kid_13_feasible () Bool)
(declare-fun title_bg_kid_12_x () Real)
(declare-fun title_bg_kid_12_width () Real)
(declare-fun title_bg_kid_12_feasible () Bool)
(declare-fun title_bg_kid_11_width () Real)
(declare-fun title_bg_kid_11_x () Real)
(declare-fun title_bg_kid_11_feasible () Bool)
(declare-fun title_bg_kid_10_width () Real)
(declare-fun title_bg_kid_10_x () Real)
(declare-fun title_bg_kid_10_feasible () Bool)
(declare-fun title_bg_kid_9_width () Real)
(declare-fun title_bg_kid_9_x () Real)
(declare-fun title_bg_kid_9_feasible () Bool)
(declare-fun title_bg_kid_8_width () Real)
(declare-fun title_bg_kid_8_x () Real)
(declare-fun title_bg_kid_8_feasible () Bool)
(declare-fun title_bg_kid_7_x () Real)
(declare-fun title_bg_kid_7_width () Real)
(declare-fun title_bg_kid_7_feasible () Bool)
(declare-fun title_bg_kid_6_width () Real)
(declare-fun title_bg_kid_6_x () Real)
(declare-fun title_bg_kid_6_feasible () Bool)
(declare-fun title_bg_kid_5_x () Real)
(declare-fun title_bg_kid_5_width () Real)
(declare-fun title_bg_kid_5_feasible () Bool)
(declare-fun title_bg_kid_4_width () Real)
(declare-fun title_bg_kid_4_x () Real)
(declare-fun title_bg_kid_4_feasible () Bool)
(declare-fun title_bg_kid_3_width () Real)
(declare-fun title_bg_kid_3_x () Real)
(declare-fun title_bg_kid_3_feasible () Bool)
(declare-fun title_bg_kid_2_width () Real)
(declare-fun title_bg_kid_2_x () Real)
(declare-fun title_bg_kid_2_feasible () Bool)
(declare-fun title_bg_kid_1_width () Real)
(declare-fun title_bg_kid_1_x () Real)
(declare-fun title_bg_kid_1_feasible () Bool)
(declare-fun title_bg_kid_0_x () Real)
(declare-fun title_bg_kid_0_width () Real)
(declare-fun title_bg_kid_0_feasible () Bool)
(declare-fun title_bg_kid_16_y () Real)
(declare-fun title_bg_hight () Real)
(declare-fun title_bg_kid_16_hight () Real)
(declare-fun title_bg_kid_15_y () Real)
(declare-fun title_bg_kid_15_hight () Real)
(declare-fun title_bg_kid_14_y () Real)
(declare-fun title_bg_kid_14_hight () Real)
(declare-fun title_bg_kid_13_y () Real)
(declare-fun title_bg_kid_13_hight () Real)
(declare-fun title_bg_kid_12_y () Real)
(declare-fun title_bg_kid_12_hight () Real)
(declare-fun title_bg_kid_11_y () Real)
(declare-fun title_bg_kid_11_hight () Real)
(declare-fun title_bg_kid_10_y () Real)
(declare-fun title_bg_kid_10_hight () Real)
(declare-fun title_bg_kid_9_y () Real)
(declare-fun title_bg_kid_9_hight () Real)
(declare-fun title_bg_kid_8_y () Real)
(declare-fun title_bg_kid_8_hight () Real)
(declare-fun title_bg_kid_7_y () Real)
(declare-fun title_bg_kid_7_hight () Real)
(declare-fun title_bg_kid_6_y () Real)
(declare-fun title_bg_kid_6_hight () Real)
(declare-fun title_bg_kid_5_y () Real)
(declare-fun title_bg_kid_5_hight () Real)
(declare-fun title_bg_kid_4_y () Real)
(declare-fun title_bg_kid_4_hight () Real)
(declare-fun title_bg_kid_3_y () Real)
(declare-fun title_bg_kid_3_hight () Real)
(declare-fun title_bg_kid_2_y () Real)
(declare-fun title_bg_kid_2_hight () Real)
(declare-fun title_bg_kid_1_y () Real)
(declare-fun title_bg_kid_1_hight () Real)
(declare-fun title_bg_kid_0_hight () Real)
(declare-fun title_bg_kid_0_y () Real)
(assert
 (let (($x5515 (<= (- (+ title_bg_kid_16_x title_bg_kid_16_width) title_bg_width) 0.0)))
 (let (($x5518 (not title_bg_kid_16_feasible)))
 (let (($x5519 (or $x5518 $x5515)))
 (let (($x5517 (or (not $x5515) title_bg_kid_16_feasible)))
 (let (($x5508 (<= (- (+ title_bg_kid_15_x title_bg_kid_15_width) title_bg_width) 0.0)))
 (let (($x5511 (not title_bg_kid_15_feasible)))
 (let (($x5512 (or $x5511 $x5508)))
 (let (($x5510 (or (not $x5508) title_bg_kid_15_feasible)))
 (let (($x5501 (<= (+ (- title_bg_kid_14_x title_bg_width) title_bg_kid_14_width) 0.0)))
 (let (($x5504 (not title_bg_kid_14_feasible)))
 (let (($x5505 (or $x5504 $x5501)))
 (let (($x5503 (or (not $x5501) title_bg_kid_14_feasible)))
 (let (($x5494 (<= (+ (- title_bg_kid_13_width title_bg_width) title_bg_kid_13_x) 0.0)))
 (let (($x5497 (not title_bg_kid_13_feasible)))
 (let (($x5498 (or $x5497 $x5494)))
 (let (($x5496 (or (not $x5494) title_bg_kid_13_feasible)))
 (let (($x5487 (<= (+ (- title_bg_kid_12_width title_bg_width) title_bg_kid_12_x) 0.0)))
 (let (($x5490 (not title_bg_kid_12_feasible)))
 (let (($x5491 (or $x5490 $x5487)))
 (let (($x5489 (or (not $x5487) title_bg_kid_12_feasible)))
 (let (($x5480 (<= (- (+ title_bg_kid_11_x title_bg_kid_11_width) title_bg_width) 0.0)))
 (let (($x5483 (not title_bg_kid_11_feasible)))
 (let (($x5484 (or $x5483 $x5480)))
 (let (($x5482 (or (not $x5480) title_bg_kid_11_feasible)))
 (let (($x5473 (<= (- (+ title_bg_kid_10_x title_bg_kid_10_width) title_bg_width) 0.0)))
 (let (($x5476 (not title_bg_kid_10_feasible)))
 (let (($x5477 (or $x5476 $x5473)))
 (let (($x5475 (or (not $x5473) title_bg_kid_10_feasible)))
 (let (($x5466 (<= (- (+ title_bg_kid_9_x title_bg_kid_9_width) title_bg_width) 0.0)))
 (let (($x5469 (not title_bg_kid_9_feasible)))
 (let (($x5470 (or $x5469 $x5466)))
 (let (($x5468 (or (not $x5466) title_bg_kid_9_feasible)))
 (let (($x5459 (<= (- (+ title_bg_kid_8_x title_bg_kid_8_width) title_bg_width) 0.0)))
 (let (($x5462 (not title_bg_kid_8_feasible)))
 (let (($x5463 (or $x5462 $x5459)))
 (let (($x5461 (or (not $x5459) title_bg_kid_8_feasible)))
 (let (($x5452 (<= (- (+ title_bg_kid_7_width title_bg_kid_7_x) title_bg_width) 0.0)))
 (let (($x5455 (not title_bg_kid_7_feasible)))
 (let (($x5456 (or $x5455 $x5452)))
 (let (($x5454 (or (not $x5452) title_bg_kid_7_feasible)))
 (let (($x5445 (<= (- (+ title_bg_kid_6_x title_bg_kid_6_width) title_bg_width) 0.0)))
 (let (($x5448 (not title_bg_kid_6_feasible)))
 (let (($x5449 (or $x5448 $x5445)))
 (let (($x5447 (or (not $x5445) title_bg_kid_6_feasible)))
 (let (($x5438 (<= (+ (- title_bg_kid_5_width title_bg_width) title_bg_kid_5_x) 0.0)))
 (let (($x5441 (not title_bg_kid_5_feasible)))
 (let (($x5442 (or $x5441 $x5438)))
 (let (($x5440 (or (not $x5438) title_bg_kid_5_feasible)))
 (let (($x5431 (<= (- (+ title_bg_kid_4_x title_bg_kid_4_width) title_bg_width) 0.0)))
 (let (($x5434 (not title_bg_kid_4_feasible)))
 (let (($x5435 (or $x5434 $x5431)))
 (let (($x5433 (or (not $x5431) title_bg_kid_4_feasible)))
 (let (($x5424 (<= (- (+ title_bg_kid_3_x title_bg_kid_3_width) title_bg_width) 0.0)))
 (let (($x5427 (not title_bg_kid_3_feasible)))
 (let (($x5428 (or $x5427 $x5424)))
 (let (($x5426 (or (not $x5424) title_bg_kid_3_feasible)))
 (let (($x5417 (<= (- (+ title_bg_kid_2_x title_bg_kid_2_width) title_bg_width) 0.0)))
 (let (($x5420 (not title_bg_kid_2_feasible)))
 (let (($x5421 (or $x5420 $x5417)))
 (let (($x5419 (or (not $x5417) title_bg_kid_2_feasible)))
 (let (($x5410 (<= (- (+ title_bg_kid_1_x title_bg_kid_1_width) title_bg_width) 0.0)))
 (let (($x5413 (not title_bg_kid_1_feasible)))
 (let (($x5414 (or $x5413 $x5410)))
 (let (($x5412 (or (not $x5410) title_bg_kid_1_feasible)))
 (let (($x5403 (<= (- (+ title_bg_kid_0_width title_bg_kid_0_x) title_bg_width) 0.0)))
 (let (($x5406 (not title_bg_kid_0_feasible)))
 (let (($x5407 (or $x5406 $x5403)))
 (let (($x5405 (or (not $x5403) title_bg_kid_0_feasible)))
 (let ((?x5399 (- (- (+ (- 10.0) title_bg_kid_16_x) title_bg_kid_15_x) title_bg_kid_15_width)))
 (let (($x5400 (= ?x5399 0.0)))
 (let ((?x5395 (- (- (+ (- 10.0) title_bg_kid_15_x) title_bg_kid_14_x) title_bg_kid_14_width)))
 (let (($x5396 (= ?x5395 0.0)))
 (let ((?x5391 (- (+ (- (- 10.0) title_bg_kid_13_width) title_bg_kid_14_x) title_bg_kid_13_x)))
 (let (($x5392 (= ?x5391 0.0)))
 (let ((?x5387 (+ (- (- (- 10.0) title_bg_kid_12_width) title_bg_kid_12_x) title_bg_kid_13_x)))
 (let (($x5388 (= ?x5387 0.0)))
 (let ((?x5383 (+ (- (- (- 10.0) title_bg_kid_11_x) title_bg_kid_11_width) title_bg_kid_12_x)))
 (let (($x5384 (= ?x5383 0.0)))
 (let ((?x5379 (- (- (+ (- 10.0) title_bg_kid_11_x) title_bg_kid_10_x) title_bg_kid_10_width)))
 (let (($x5380 (= ?x5379 0.0)))
 (let ((?x5375 (- (+ (- (- 10.0) title_bg_kid_9_x) title_bg_kid_10_x) title_bg_kid_9_width)))
 (let (($x5376 (= ?x5375 0.0)))
 (let ((?x5371 (- (- (+ (- 10.0) title_bg_kid_9_x) title_bg_kid_8_x) title_bg_kid_8_width)))
 (let (($x5372 (= ?x5371 0.0)))
 (let ((?x5367 (- (+ (- (- 10.0) title_bg_kid_7_width) title_bg_kid_8_x) title_bg_kid_7_x)))
 (let (($x5368 (= ?x5367 0.0)))
 (let ((?x5363 (+ (- (- (- 10.0) title_bg_kid_6_x) title_bg_kid_6_width) title_bg_kid_7_x)))
 (let (($x5364 (= ?x5363 0.0)))
 (let ((?x5359 (- (- (+ (- 10.0) title_bg_kid_6_x) title_bg_kid_5_width) title_bg_kid_5_x)))
 (let (($x5360 (= ?x5359 0.0)))
 (let ((?x5355 (+ (- (- (- 10.0) title_bg_kid_4_x) title_bg_kid_4_width) title_bg_kid_5_x)))
 (let (($x5356 (= ?x5355 0.0)))
 (let ((?x5351 (- (- (+ (- 10.0) title_bg_kid_4_x) title_bg_kid_3_x) title_bg_kid_3_width)))
 (let (($x5352 (= ?x5351 0.0)))
 (let ((?x5347 (- (+ (- (- 10.0) title_bg_kid_2_x) title_bg_kid_3_x) title_bg_kid_2_width)))
 (let (($x5348 (= ?x5347 0.0)))
 (let ((?x5343 (- (- (+ (- 10.0) title_bg_kid_2_x) title_bg_kid_1_x) title_bg_kid_1_width)))
 (let (($x5344 (= ?x5343 0.0)))
 (let ((?x5339 (- (+ (- (- 10.0) title_bg_kid_0_width) title_bg_kid_1_x) title_bg_kid_0_x)))
 (let (($x5340 (= ?x5339 0.0)))
 (let (($x5336 (= title_bg_kid_16_y 10.0)))
 (let (($x5335 (= (+ (- title_bg_kid_16_hight title_bg_hight) title_bg_kid_16_y) (- 10.0))))
 (let (($x5332 (= title_bg_kid_15_y 10.0)))
 (let (($x5331 (= (- (+ title_bg_kid_15_y title_bg_kid_15_hight) title_bg_hight) (- 10.0))))
 (let (($x5328 (= title_bg_kid_14_y 10.0)))
 (let (($x5327 (= (+ (- title_bg_kid_14_y title_bg_hight) title_bg_kid_14_hight) (- 10.0))))
 (let (($x5324 (= title_bg_kid_13_y 10.0)))
 (let (($x5323 (= (+ (+ (- title_bg_hight) title_bg_kid_13_y) title_bg_kid_13_hight) (- 10.0))))
 (let (($x5320 (= title_bg_kid_12_y 10.0)))
 (let (($x5319 (= (+ (+ (- title_bg_hight) title_bg_kid_12_y) title_bg_kid_12_hight) (- 10.0))))
 (let (($x5316 (= title_bg_kid_11_y 10.0)))
 (let (($x5315 (= (+ (- title_bg_kid_11_hight title_bg_hight) title_bg_kid_11_y) (- 10.0))))
 (let (($x5312 (= title_bg_kid_10_y 10.0)))
 (let (($x5311 (= (+ (- title_bg_kid_10_hight title_bg_hight) title_bg_kid_10_y) (- 10.0))))
 (let (($x5308 (= title_bg_kid_9_y 10.0)))
 (let (($x5307 (= (+ (- title_bg_kid_9_hight title_bg_hight) title_bg_kid_9_y) (- 10.0))))
 (let (($x5304 (= title_bg_kid_8_y 10.0)))
 (let (($x5303 (= (- (+ title_bg_kid_8_y title_bg_kid_8_hight) title_bg_hight) (- 10.0))))
 (let (($x5300 (= title_bg_kid_7_y 10.0)))
 (let (($x5299 (= (+ (- title_bg_kid_7_y title_bg_hight) title_bg_kid_7_hight) (- 10.0))))
 (let (($x5296 (= title_bg_kid_6_y 10.0)))
 (let (($x5295 (= (+ (+ (- title_bg_hight) title_bg_kid_6_y) title_bg_kid_6_hight) (- 10.0))))
 (let (($x5292 (= title_bg_kid_5_y 10.0)))
 (let (($x5291 (= (+ (+ (- title_bg_hight) title_bg_kid_5_y) title_bg_kid_5_hight) (- 10.0))))
 (let (($x5288 (= title_bg_kid_4_y 10.0)))
 (let (($x5287 (= (+ (+ (- title_bg_hight) title_bg_kid_4_y) title_bg_kid_4_hight) (- 10.0))))
 (let (($x5283 (= title_bg_kid_3_y 10.0)))
 (let (($x5282 (= (+ (- title_bg_kid_3_hight title_bg_hight) title_bg_kid_3_y) (- 10.0))))
 (let (($x5279 (= title_bg_kid_2_y 10.0)))
 (let (($x5278 (= (+ (- title_bg_kid_2_hight title_bg_hight) title_bg_kid_2_y) (- 10.0))))
 (let (($x5275 (= title_bg_kid_1_y 10.0)))
 (let (($x5274 (= (- (+ title_bg_kid_1_y title_bg_kid_1_hight) title_bg_hight) (- 10.0))))
 (let (($x5271 (= (+ (- title_bg_kid_0_y title_bg_hight) title_bg_kid_0_hight) (- 10.0))))
 (let (($x5268 (= title_bg_kid_0_y 10.0)))
 (let (($x5267 (= title_bg_kid_0_x 10.0)))
 (let (($x5266 (= title_bg_kid_16_width 100.0)))
 (let (($x5265 (= title_bg_kid_15_width 100.0)))
 (let (($x5264 (= title_bg_kid_14_width 100.0)))
 (let (($x5263 (= title_bg_kid_13_width 100.0)))
 (let (($x5262 (= title_bg_kid_12_width 100.0)))
 (let (($x5261 (= title_bg_kid_11_width 100.0)))
 (let (($x5260 (= title_bg_kid_10_width 100.0)))
 (let (($x5259 (= title_bg_kid_9_width 100.0)))
 (let (($x5258 (= title_bg_kid_8_width 100.0)))
 (let (($x5257 (= title_bg_kid_7_width 100.0)))
 (let (($x5256 (= title_bg_kid_6_width 100.0)))
 (let (($x5255 (= title_bg_kid_5_width 100.0)))
 (let (($x5254 (= title_bg_kid_4_width 100.0)))
 (let (($x5253 (= title_bg_kid_3_width 100.0)))
 (let (($x5252 (= title_bg_kid_2_width 100.0)))
 (let (($x5251 (= title_bg_kid_1_width 100.0)))
 (let (($x5250 (= title_bg_kid_0_width 100.0)))
 (let (($x5248 (>= title_bg_kid_16_hight 0.0)))
 (let (($x5247 (>= title_bg_kid_16_width 0.0)))
 (let (($x5246 (>= title_bg_kid_16_y 0.0)))
 (let (($x5245 (>= title_bg_kid_16_x 0.0)))
 (let (($x5244 (>= title_bg_kid_15_hight 0.0)))
 (let (($x5243 (>= title_bg_kid_15_width 0.0)))
 (let (($x5242 (>= title_bg_kid_15_y 0.0)))
 (let (($x5241 (>= title_bg_kid_15_x 0.0)))
 (let (($x5240 (>= title_bg_kid_14_hight 0.0)))
 (let (($x5239 (>= title_bg_kid_14_width 0.0)))
 (let (($x5238 (>= title_bg_kid_14_y 0.0)))
 (let (($x5237 (>= title_bg_kid_14_x 0.0)))
 (let (($x5236 (>= title_bg_kid_13_hight 0.0)))
 (let (($x5235 (>= title_bg_kid_13_width 0.0)))
 (let (($x5234 (>= title_bg_kid_13_y 0.0)))
 (let (($x5233 (>= title_bg_kid_13_x 0.0)))
 (let (($x5232 (>= title_bg_kid_12_hight 0.0)))
 (let (($x5231 (>= title_bg_kid_12_width 0.0)))
 (let (($x5230 (>= title_bg_kid_12_y 0.0)))
 (let (($x5229 (>= title_bg_kid_12_x 0.0)))
 (let (($x5228 (>= title_bg_kid_11_hight 0.0)))
 (let (($x5227 (>= title_bg_kid_11_width 0.0)))
 (let (($x5226 (>= title_bg_kid_11_y 0.0)))
 (let (($x5225 (>= title_bg_kid_11_x 0.0)))
 (let (($x5224 (>= title_bg_kid_10_hight 0.0)))
 (let (($x5223 (>= title_bg_kid_10_width 0.0)))
 (let (($x5222 (>= title_bg_kid_10_y 0.0)))
 (let (($x5221 (>= title_bg_kid_10_x 0.0)))
 (let (($x5220 (>= title_bg_kid_9_hight 0.0)))
 (let (($x5219 (>= title_bg_kid_9_width 0.0)))
 (let (($x5218 (>= title_bg_kid_9_y 0.0)))
 (let (($x5217 (>= title_bg_kid_9_x 0.0)))
 (let (($x5216 (>= title_bg_kid_8_hight 0.0)))
 (let (($x5215 (>= title_bg_kid_8_width 0.0)))
 (let (($x5214 (>= title_bg_kid_8_y 0.0)))
 (let (($x5213 (>= title_bg_kid_8_x 0.0)))
 (let (($x5212 (>= title_bg_kid_7_hight 0.0)))
 (let (($x5211 (>= title_bg_kid_7_width 0.0)))
 (let (($x5210 (>= title_bg_kid_7_y 0.0)))
 (let (($x5209 (>= title_bg_kid_7_x 0.0)))
 (let (($x5208 (>= title_bg_kid_6_hight 0.0)))
 (let (($x5207 (>= title_bg_kid_6_width 0.0)))
 (let (($x5206 (>= title_bg_kid_6_y 0.0)))
 (let (($x5205 (>= title_bg_kid_6_x 0.0)))
 (let (($x5204 (>= title_bg_kid_5_hight 0.0)))
 (let (($x5203 (>= title_bg_kid_5_width 0.0)))
 (let (($x5202 (>= title_bg_kid_5_y 0.0)))
 (let (($x5201 (>= title_bg_kid_5_x 0.0)))
 (let (($x5200 (>= title_bg_kid_4_hight 0.0)))
 (let (($x5199 (>= title_bg_kid_4_width 0.0)))
 (let (($x5198 (>= title_bg_kid_4_y 0.0)))
 (let (($x5197 (>= title_bg_kid_4_x 0.0)))
 (let (($x5196 (>= title_bg_kid_3_hight 0.0)))
 (let (($x5195 (>= title_bg_kid_3_width 0.0)))
 (let (($x5194 (>= title_bg_kid_3_y 0.0)))
 (let (($x5193 (>= title_bg_kid_3_x 0.0)))
 (let (($x5192 (>= title_bg_kid_2_hight 0.0)))
 (let (($x5191 (>= title_bg_kid_2_width 0.0)))
 (let (($x5190 (>= title_bg_kid_2_y 0.0)))
 (let (($x5189 (>= title_bg_kid_2_x 0.0)))
 (let (($x5188 (>= title_bg_kid_1_hight 0.0)))
 (let (($x5187 (>= title_bg_kid_1_width 0.0)))
 (let (($x5186 (>= title_bg_kid_1_y 0.0)))
 (let (($x5185 (>= title_bg_kid_1_x 0.0)))
 (let (($x5184 (>= title_bg_kid_0_hight 0.0)))
 (let (($x5183 (>= title_bg_kid_0_width 0.0)))
 (let (($x5182 (>= title_bg_kid_0_y 0.0)))
 (let (($x5181 (>= title_bg_kid_0_x 0.0)))
 (and $x5181 $x5182 $x5183 $x5184 $x5185 $x5186 $x5187 $x5188 $x5189 $x5190 $x5191 $x5192 $x5193 $x5194 $x5195 $x5196 $x5197 $x5198 $x5199 $x5200 $x5201 $x5202 $x5203 $x5204 $x5205 $x5206 $x5207 $x5208 $x5209 $x5210 $x5211 $x5212 $x5213 $x5214 $x5215 $x5216 $x5217 $x5218 $x5219 $x5220 $x5221 $x5222 $x5223 $x5224 $x5225 $x5226 $x5227 $x5228 $x5229 $x5230 $x5231 $x5232 $x5233 $x5234 $x5235 $x5236 $x5237 $x5238 $x5239 $x5240 $x5241 $x5242 $x5243 $x5244 $x5245 $x5246 $x5247 $x5248 $x5250 $x5251 $x5252 $x5253 $x5254 $x5255 $x5256 $x5257 $x5258 $x5259 $x5260 $x5261 $x5262 $x5263 $x5264 $x5265 $x5266 $x5267 $x5268 $x5271 $x5274 $x5275 $x5278 $x5279 $x5282 $x5283 $x5287 $x5288 $x5291 $x5292 $x5295 $x5296 $x5299 $x5300 $x5303 $x5304 $x5307 $x5308 $x5311 $x5312 $x5315 $x5316 $x5319 $x5320 $x5323 $x5324 $x5327 $x5328 $x5331 $x5332 $x5335 $x5336 $x5340 $x5344 $x5348 $x5352 $x5356 $x5360 $x5364 $x5368 $x5372 $x5376 $x5380 $x5384 $x5388 $x5392 $x5396 $x5400 $x5405 $x5407 $x5412 $x5414 $x5419 $x5421 $x5426 $x5428 $x5433 $x5435 $x5440 $x5442 $x5447 $x5449 $x5454 $x5456 $x5461 $x5463 $x5468 $x5470 $x5475 $x5477 $x5482 $x5484 $x5489 $x5491 $x5496 $x5498 $x5503 $x5505 $x5510 $x5512 $x5517 $x5519 title_bg_feasible))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

